$\forall$$A$:es\_realizer\{i:l\}, $P$:(ES\{i\}$\rightarrow$Prop$_{\mbox{\scriptsize i'}}$).
\\[0ex]($\forall$${\it es}$:ES\{i\}. $P$(${\it es}$)) $\Rightarrow$ R{-}Feasible\{i:l\}($A$) $\Rightarrow$ $A$ $\Vdash$\{i\} ${\it es}$.$P$(${\it es}$)